M1, M2:MsgA. M1 ||decl M2  M1  M2  MsgA 

latex

Definitions

t  T, KindDeq, Knd, Type, x.A(x), P  Q, x:A. B(x), x. t(x), f  g, IdLnk, 2of(t), rcv(l,tg), f  g, Void, 1of(t), Top, IdDeq, Id, f(x)?z, type List, State(ds), x:AB(x), x:AB(x), a:A fp B(a), x:A. B(x), f || g, locl(a), Prop, Valtype(da;k), P & Q, IdLnkDeq, product-deq(A;B;a;b), mk-ma, MsgA, M1  M2, M1 ||decl M2

Lemmas

msga wf, mk-ma wf, ma-valtype wf, product-deq wf, idlnk-deq wf, fpf-trivial-subtype-top, fpf-compatible wf, locl wf, fpf-sub-join-left, fpf wf, subtype-fpf2, subtype rel product, ma-state wf, subtype rel dep function, subtype rel self, subtype rel function, subtype rel list, fpf-cap wf, Id wf, id-deq wf, subtype-fpf-cap-top, top wf, pi1 wf, subtype-fpf-cap-void, fpf-join wf, rcv wf, pi2 wf, IdLnk wf, fpf-sub-join-right, Knd wf, Kind-deq wf